0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 90 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 76 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 PiDPToQDPProof (⇒, 0 ms)
↳9 QDP
↳10 MRRProof (⇔, 125 ms)
↳11 QDP
↳12 DependencyGraphProof (⇔, 0 ms)
↳13 TRUE
↳14 PiDP
↳15 PiDPToQDPProof (⇒, 0 ms)
↳16 QDP
↳17 MRRProof (⇔, 0 ms)
↳18 QDP
↳19 DependencyGraphProof (⇔, 0 ms)
↳20 TRUE
FC_IN_GAA(s(X1), X2, X3) → U7_GAA(X1, X2, X3, pA_in_gaaa(X1, X2, X4, X3))
FC_IN_GAA(s(X1), X2, X3) → PA_IN_GAAA(X1, X2, X4, X3)
PA_IN_GAAA(s(X1), X2, X3, X4) → U1_GAAA(X1, X2, X3, X4, fB_in_gaa(X1, X2, X5))
PA_IN_GAAA(s(X1), X2, X3, X4) → FB_IN_GAA(X1, X2, X5)
FB_IN_GAA(s(X1), X2, X3) → U4_GAA(X1, X2, X3, fB_in_gaa(X1, X2, X4))
FB_IN_GAA(s(X1), X2, X3) → FB_IN_GAA(X1, X2, X4)
FB_IN_GAA(s(X1), X2, X3) → U5_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U6_GAA(X1, X2, X3, fB_in_gaa(X4, X2, X3))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FB_IN_GAA(X4, X2, X3)
PA_IN_GAAA(s(X1), X2, X3, X4) → U2_GAAA(X1, X2, X3, X4, fcB_in_gaa(X1, X2, X5))
U2_GAAA(X1, X2, X3, X4, fcB_out_gaa(X1, X2, X5)) → U3_GAAA(X1, X2, X3, X4, pA_in_gaaa(X5, X2, X3, X4))
U2_GAAA(X1, X2, X3, X4, fcB_out_gaa(X1, X2, X5)) → PA_IN_GAAA(X5, X2, X3, X4)
fcB_in_gaa(0, X1, 0) → fcB_out_gaa(0, X1, 0)
fcB_in_gaa(s(X1), X2, X3) → U11_gaa(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U11_gaa(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U12_gaa(X1, X2, X3, X4, fcB_in_gaa(X4, X2, X3))
U12_gaa(X1, X2, X3, X4, fcB_out_gaa(X4, X2, X3)) → fcB_out_gaa(s(X1), X2, X3)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
FC_IN_GAA(s(X1), X2, X3) → U7_GAA(X1, X2, X3, pA_in_gaaa(X1, X2, X4, X3))
FC_IN_GAA(s(X1), X2, X3) → PA_IN_GAAA(X1, X2, X4, X3)
PA_IN_GAAA(s(X1), X2, X3, X4) → U1_GAAA(X1, X2, X3, X4, fB_in_gaa(X1, X2, X5))
PA_IN_GAAA(s(X1), X2, X3, X4) → FB_IN_GAA(X1, X2, X5)
FB_IN_GAA(s(X1), X2, X3) → U4_GAA(X1, X2, X3, fB_in_gaa(X1, X2, X4))
FB_IN_GAA(s(X1), X2, X3) → FB_IN_GAA(X1, X2, X4)
FB_IN_GAA(s(X1), X2, X3) → U5_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U6_GAA(X1, X2, X3, fB_in_gaa(X4, X2, X3))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FB_IN_GAA(X4, X2, X3)
PA_IN_GAAA(s(X1), X2, X3, X4) → U2_GAAA(X1, X2, X3, X4, fcB_in_gaa(X1, X2, X5))
U2_GAAA(X1, X2, X3, X4, fcB_out_gaa(X1, X2, X5)) → U3_GAAA(X1, X2, X3, X4, pA_in_gaaa(X5, X2, X3, X4))
U2_GAAA(X1, X2, X3, X4, fcB_out_gaa(X1, X2, X5)) → PA_IN_GAAA(X5, X2, X3, X4)
fcB_in_gaa(0, X1, 0) → fcB_out_gaa(0, X1, 0)
fcB_in_gaa(s(X1), X2, X3) → U11_gaa(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U11_gaa(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U12_gaa(X1, X2, X3, X4, fcB_in_gaa(X4, X2, X3))
U12_gaa(X1, X2, X3, X4, fcB_out_gaa(X4, X2, X3)) → fcB_out_gaa(s(X1), X2, X3)
FB_IN_GAA(s(X1), X2, X3) → U5_GAA(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U5_GAA(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → FB_IN_GAA(X4, X2, X3)
FB_IN_GAA(s(X1), X2, X3) → FB_IN_GAA(X1, X2, X4)
fcB_in_gaa(0, X1, 0) → fcB_out_gaa(0, X1, 0)
fcB_in_gaa(s(X1), X2, X3) → U11_gaa(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U11_gaa(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U12_gaa(X1, X2, X3, X4, fcB_in_gaa(X4, X2, X3))
U12_gaa(X1, X2, X3, X4, fcB_out_gaa(X4, X2, X3)) → fcB_out_gaa(s(X1), X2, X3)
FB_IN_GAA(s(X1)) → U5_GAA(X1, fcB_in_gaa(X1))
U5_GAA(X1, fcB_out_gaa(X1, X4)) → FB_IN_GAA(X4)
FB_IN_GAA(s(X1)) → FB_IN_GAA(X1)
fcB_in_gaa(0) → fcB_out_gaa(0, 0)
fcB_in_gaa(s(X1)) → U11_gaa(X1, fcB_in_gaa(X1))
U11_gaa(X1, fcB_out_gaa(X1, X4)) → U12_gaa(X1, fcB_in_gaa(X4))
U12_gaa(X1, fcB_out_gaa(X4, X3)) → fcB_out_gaa(s(X1), X3)
fcB_in_gaa(x0)
U11_gaa(x0, x1)
U12_gaa(x0, x1)
FB_IN_GAA(s(X1)) → U5_GAA(X1, fcB_in_gaa(X1))
FB_IN_GAA(s(X1)) → FB_IN_GAA(X1)
POL(0) = 0
POL(FB_IN_GAA(x1)) = 2 + 2·x1
POL(U11_gaa(x1, x2)) = 1 + x1 + x2
POL(U12_gaa(x1, x2)) = 1 + 2·x1 + x2
POL(U5_GAA(x1, x2)) = 2 + 2·x1 + 2·x2
POL(fcB_in_gaa(x1)) = x1
POL(fcB_out_gaa(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + 2·x1
U5_GAA(X1, fcB_out_gaa(X1, X4)) → FB_IN_GAA(X4)
fcB_in_gaa(0) → fcB_out_gaa(0, 0)
fcB_in_gaa(s(X1)) → U11_gaa(X1, fcB_in_gaa(X1))
U11_gaa(X1, fcB_out_gaa(X1, X4)) → U12_gaa(X1, fcB_in_gaa(X4))
U12_gaa(X1, fcB_out_gaa(X4, X3)) → fcB_out_gaa(s(X1), X3)
fcB_in_gaa(x0)
U11_gaa(x0, x1)
U12_gaa(x0, x1)
PA_IN_GAAA(s(X1), X2, X3, X4) → U2_GAAA(X1, X2, X3, X4, fcB_in_gaa(X1, X2, X5))
U2_GAAA(X1, X2, X3, X4, fcB_out_gaa(X1, X2, X5)) → PA_IN_GAAA(X5, X2, X3, X4)
fcB_in_gaa(0, X1, 0) → fcB_out_gaa(0, X1, 0)
fcB_in_gaa(s(X1), X2, X3) → U11_gaa(X1, X2, X3, fcB_in_gaa(X1, X2, X4))
U11_gaa(X1, X2, X3, fcB_out_gaa(X1, X2, X4)) → U12_gaa(X1, X2, X3, X4, fcB_in_gaa(X4, X2, X3))
U12_gaa(X1, X2, X3, X4, fcB_out_gaa(X4, X2, X3)) → fcB_out_gaa(s(X1), X2, X3)
PA_IN_GAAA(s(X1)) → U2_GAAA(X1, fcB_in_gaa(X1))
U2_GAAA(X1, fcB_out_gaa(X1, X5)) → PA_IN_GAAA(X5)
fcB_in_gaa(0) → fcB_out_gaa(0, 0)
fcB_in_gaa(s(X1)) → U11_gaa(X1, fcB_in_gaa(X1))
U11_gaa(X1, fcB_out_gaa(X1, X4)) → U12_gaa(X1, fcB_in_gaa(X4))
U12_gaa(X1, fcB_out_gaa(X4, X3)) → fcB_out_gaa(s(X1), X3)
fcB_in_gaa(x0)
U11_gaa(x0, x1)
U12_gaa(x0, x1)
PA_IN_GAAA(s(X1)) → U2_GAAA(X1, fcB_in_gaa(X1))
POL(0) = 0
POL(PA_IN_GAAA(x1)) = 2 + 2·x1
POL(U11_gaa(x1, x2)) = 1 + x1 + x2
POL(U12_gaa(x1, x2)) = 1 + 2·x1 + 2·x2
POL(U2_GAAA(x1, x2)) = 2 + x1 + 2·x2
POL(fcB_in_gaa(x1)) = x1
POL(fcB_out_gaa(x1, x2)) = x1 + 2·x2
POL(s(x1)) = 1 + 2·x1
U2_GAAA(X1, fcB_out_gaa(X1, X5)) → PA_IN_GAAA(X5)
fcB_in_gaa(0) → fcB_out_gaa(0, 0)
fcB_in_gaa(s(X1)) → U11_gaa(X1, fcB_in_gaa(X1))
U11_gaa(X1, fcB_out_gaa(X1, X4)) → U12_gaa(X1, fcB_in_gaa(X4))
U12_gaa(X1, fcB_out_gaa(X4, X3)) → fcB_out_gaa(s(X1), X3)
fcB_in_gaa(x0)
U11_gaa(x0, x1)
U12_gaa(x0, x1)